the_w:World, e, e':E. (e = e')  (e = e') 

latex

Definitions	x:A. B(x), E, P  Q, p = q, P & Q, , t  T, x. t(x), , P  Q, x(s), A, t.1, t.2, A  B, False
Lemmas	iff transitivity, assert wf, assert of band, and functionality wrt iff, assert-eq-id, assert of eq int, band wf, eq id wf, pi1 wf, Id wf, nat wf, eq int wf, pi2 wf, not wf, w-isnull wf, w-a wf, world wf, le wf